Upstream first batch of lemmas from Lido engagement#2787
Conversation
| rule 0 <Int X => true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)] | ||
|
|
||
| rule X <=Int maxUInt256 => X <Int pow256 [simplification] | ||
|
|
There was a problem hiding this comment.
Not entirely sure these three lemmas are strictly necessary. They seem to be things that the SMT solver could easily resolve, but maybe they can help trigger further simplifications.
| andBool 0 <Int C | ||
| andBool A <Int ( C *Int B ) | ||
| [simplification, symbolic(A, B), concrete(C), preserves-definedness] | ||
|
|
There was a problem hiding this comment.
This is a fairly specific lemma, but I suppose it might be worth having if we run into an expression like this again.
|
|
||
| rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] | ||
| rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] | ||
|
|
There was a problem hiding this comment.
Set a later priority for these rules so they don't conflict with the preceding ones.
| #asWord ( B1 +Bytes B2 ) <Int X => #asWord ( B1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) ) | ||
| requires X modInt ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) ) ==Int 0 | ||
| [simplification, preserves-definedness] | ||
|
|
There was a problem hiding this comment.
Not sure if too specific. I considered if it should use the concrete(X) attribute, but if it didn't include it in the first place it's probably because the expression that originally motivated it had a symbolic X.
| rule [b2w-lt]: | ||
| bool2Word ( B:Bool ) *Int X <Int Y => | ||
| ( ( notBool B ) andBool 0 <Int Y ) orBool ( B andBool X <Int Y ) | ||
| [simplification, concrete(Y)] |
There was a problem hiding this comment.
In the original file this had a typo, ( notBool B ) andBool 0 <=Int Y.
| X xorInt Y <Int Z => true | ||
| requires X <Int ( 2 ^Int log2Int ( Z ) ) andBool Y <Int ( 2 ^Int log2Int ( Z ) ) | ||
| [simplification, concrete(Z)] |
There was a problem hiding this comment.
Does this need an additional constraint for Z >Int 0 to avoid the log2Int undefinedness?
There was a problem hiding this comment.
Good catch, I'll add the constraint
lucasmt
force-pushed
the
upstream-lido-lemmas
branch
from
2fdfcac to
f432111
Compare
| claim [zero-lt-sub]: <k> runLemma ( 0 <Int A -Int B ) => doneLemma ( B <Int A ) ... </k> | ||
| claim [zero-le-sub]: <k> runLemma ( 0 <=Int A -Int B ) => doneLemma ( B <=Int A ) ... </k> | ||
| claim [zero-gt-sub]: <k> runLemma ( 0 >Int A -Int B ) => doneLemma ( B >Int A ) ... </k> | ||
| claim [zero-ge-sub]: <k> runLemma ( 0 >=Int A -Int B ) => doneLemma ( B >=Int A ) ... </k> | ||
|
|
||
| claim [sub-gt-zero]: <k> runLemma ( A -Int B >Int 0 ) => doneLemma ( A >Int B ) ... </k> | ||
| claim [sub-ge-zero]: <k> runLemma ( A -Int B >=Int 0 ) => doneLemma ( A >=Int B ) ... </k> | ||
| claim [sub-lt-zero]: <k> runLemma ( A -Int B <Int 0 ) => doneLemma ( A <Int B ) ... </k> | ||
| claim [sub-le-zero]: <k> runLemma ( A -Int B <=Int 0 ) => doneLemma ( A <=Int B ) ... </k> | ||
|
|
||
| claim [mul-lt-const]: <k> runLemma ( 36 *Int B <Int 1728 ) => doneLemma ( B <Int 48 ) ... </k> | ||
| claim [mul-le-const]: <k> runLemma ( 36 *Int B <=Int 1728 ) => doneLemma ( B <=Int 48 ) ... </k> | ||
| claim [mul-gt-const]: <k> runLemma ( 36 *Int B >Int 1728 ) => doneLemma ( B >Int 48 ) ... </k> | ||
| claim [mul-ge-const]: <k> runLemma ( 36 *Int B >=Int 1728 ) => doneLemma ( B >=Int 48 ) ... </k> | ||
|
|
||
| claim [const-gt-mul]: <k> runLemma ( 1728 >Int 36 *Int B ) => doneLemma ( 48 >Int B ) ... </k> | ||
| claim [const-ge-mul]: <k> runLemma ( 1728 >=Int 36 *Int B ) => doneLemma ( 48 >=Int B ) ... </k> | ||
| claim [const-lt-mul]: <k> runLemma ( 1728 <Int 36 *Int B ) => doneLemma ( 48 <Int B ) ... </k> | ||
| claim [const-le-mul]: <k> runLemma ( 1728 <=Int 36 *Int B ) => doneLemma ( 48 <=Int B ) ... </k> | ||
|
|
||
| claim [eq-neg]: <k> runLemma ( A ==Int -1 ) => doneLemma ( false ) ... </k> | ||
| requires 0 <=Int A | ||
|
|
||
| claim [nonneg-and-nonzero]: <k> runLemma ( 0 <Int X ) => doneLemma ( true ) ... </k> | ||
| requires 0 <=Int X andBool notBool ( X ==Int 0 ) | ||
|
|
||
| claim [le-maxuint256]: <k> runLemma ( X <=Int maxUInt256 ) => doneLemma ( X <Int pow256 ) ... </k> | ||
|
|
There was a problem hiding this comment.
These claims pass even without the corresponding lemmas, but only because the SMT solver can prove the implication. The lemmas are needed if we want to actually simplify the expressions.
2 participants
Lemmas were taken from this file: https://github.com/runtimeverification/_audits_lidofinance_dual-governance_fork/blob/rv-extension-refactor-full-suite/test/kontrol/lido-lemmas.k. Not all of the lemmas have been included, as some of them require further analysis.